
 \rnd is used to detect and predict toxic behaviors related to the  dynamics of bio-molecular networks. In order to verify toxicology properties, we resort to temporal logics and model checking techniques \cite{edmund}. For the sake of the present paper computation tree logic (CTL) allows to express properties of interest. Nonetheless different scenarios may require other more appropriate modal logic which we  could be  handled by our framework.

We recall here the basic concepts of CTL, we provide the formal definition of the syntax but we only give some intuitions on the semantics, which is formally defined in \cite{emerson}.

\begin{definition}[CTL]
Let $a \in A$ be an atomic proposition, a CTL formula is defined as: 
$$
\begin{array}{ll}
 \varphi::= &\bot \mid a \mid \neg \varphi \mid \varphi \vee \varphi \mid \varphi \wedge \varphi \mid \varphi \rightarrow \varphi \\
 & \esiste \x \varphi \mid \esiste \globally \varphi \mid \esiste (\varphi  \until \varphi) \mid \esiste \finally \varphi \mid \all \globally \varphi \mid \all \finally \varphi
\end{array}
 $$
\end{definition}

CTL is used to state properties on branching time structures.%: its formulae refers to multiple runs at the same time.
The logic uses usual boolean operators, path quantifiers and temporal operators. Boolean operators have the expected semantics. Path quantifiers can be of two kinds $\all$ and $\esiste$. $\all \varphi$ means  that $\varphi$ has to hold on all paths starting from the current state, while $\esiste \varphi$ stands for there exists at least one path starting from the current state where $\varphi$ holds.
We have four temporal operators: $\x, \globally, \finally$ and $\until$. 
$\x \varphi$ holds if $\varphi$ is true at the \emph{next} state. $\globally \varphi$ means  that $\varphi$ has to \emph{globally} hold on the entire subsequent path. $\finally \varphi$ stands for eventually (or \emph{finally}) $\varphi$ has to hold (at some point on the subsequent path).  And finally, $\varphi_1 \until \varphi_2$ means that $\varphi_1$ has to hold at least \emph{until} at some position $\varphi_2$ holds. 
In our context atomic formulae are represented by pairs of species and  levels: $A = \{(s, \level{s}) \mid  s\in \res\}$, for instance $(Glucose,2)$. \looseness=-1

As mentioned in the introduction, we are mainly interested in checking whether the inner equilibrium of an organism (tissue, cell, \dots) is maintained when administrating drugs or applying stressors.  More in detail, toxicology properties can be classified into two categories: i) properties  checking for the appearance  of particular symptoms, and   ii) properties characterizing causal relations between events. The former class of properties basically consists in verifying reachability of some states, while the latter  concerns pathways that highlight 
 sequences of events leading to toxic outcomes.
For instance, in the case of glucose regulation, we could verify whether  glycemia levels are kept stable and whether they change in  case of ingestion of aspartame. More precisely, we could examine the causes and the symptoms of the hypoglycemia induced by the assimilation of aspartame. Hence  hypoglycemia is treated as a toxic state. 


\begin{example}[Glucose metabolism]
Take our running example of blood glucose regulation. The following properties can be expressed in CTL:

\begin{description}
 \item[Symptoms:] Is it possible to have an anomalous decrease of glucose levels in blood (revealing hypoglycemia)? 
$$\esiste \finally (Glycemia, 0)$$
 \item [Mode-of-action:] Recalling that the blood glucose regulation process normally maintains  glycemia at equilibrium (level $2$), does it exist an abnormal behavior leading to hypoglycemia?
$$\esiste (\esiste \finally (Glycemia, 2) ~\until~ (\esiste \finally (Glycemia, 0)))$$
 \item [Causality:] Does assimilation of sweeteners cause hypoglycemia? 
$$\begin{array}{l}
\esiste \finally [((Sugar, 1) \vee (Aspartame, 1)) \wedge (Glycemia, 1)] \rightarrow  \all \finally (Glycemia,2)   
  \end{array}
 $$
\end{description}

For the third formula we  show two paths given as sequences of reactions (abstracting away from time transitions), one that satisfy the formula and the other that contradicts it.
The first one corresponds to the assimilation of sugar. As described in Section \ref{sec:example}, the digestion of sugar induces an increase of the production of insulin and an augmentation of the blood glucose levels. Nonetheless the levels of insulin produced are not enough to cause the glycemia to drop and the formula is satisfied.
$$
\begin{array}{l}
(Sugar, 1), (Aspartame, 0), (Glycemia, 1), (Insulin, 0), (Glucagon, 0) \xrightarrow{\rho_1}\\
(Sugar, 1), (Aspartame, 0), \mathbf{(Glycemia, 2)}, (Insulin, 1), (Glucagon, 0) 
\end{array}
 $$
Unlike previous path, the assimilation of aspartame causes only an increase of insulin. Unfortunately, this increment is sufficient to induce a decrease of blood glucose levels thus contradicting the formula above.
$$
\begin{array}{l}
 (Sugar, 0), (Aspartame, 1), (Glycemia, 1), (Insulin, 0), (Glucagon, 0) \xrightarrow{\rho_2} \\ 
 (Sugar, 0), (Aspartame, 1), (Glycemia, 1), (Insulin, 1), (Glucagon, 0) \xrightarrow{\rho_7} \\
 (Sugar, 0), (Aspartame, 0), \mathbf{(Glycemia, 0)}, (Insulin, 1), (Glucagon, 0)
\end{array}
 $$
%This illustrates the toxic behavior caused by aspartame described in Section \ref{sec:example}. 
\hfill $\diamond$
\end{example}

In order to automatically verify  satisfiability of formulae, we  build  from \rnd a suitable Kripke structure $K$. Informally,  $K$ is a variant of finite state machine where each state $v$ has at least one successor and $v$ is labeled with the set of atomic formulae true in $v$. 
We recall the definition of Kripke structure \cite{kripke}: 

\begin{definition}[Kripke structure]
Let $A$ be a set of atomic formulae, a \emph{Kripke structure} over $A$ is a tuple $K = (V, v_0, \longrightarrow, \lab)$ where $V$ is a finite set of states, $v_0\in V$ is the initial state,  $\longrightarrow \subset V \times V$ is a left total transition relation (meaning that $\forall v\in V,  \exists v' \in V$ such that $v \longrightarrow v'$) and $\lab$ is the labeling  function on states $\lab: V \to 2^{A}$. 
\end{definition}

\subsubsection*{Abstraction for the verification.} Notice that \rnd networks have an unbounded state space as the clock can be incremented unboundedly. In order to obtain a Kripke structure representation of \rnd networks, we need to find a suitable abstraction.  
We observe that changes in the status of species are referred to discrete intervals of time thereby in the abstraction we %are not interested in the actual value of the clock $z$ but 
refer only to the relative duration of reactions or decay processes.  
For instance, in \rnd,  to determine whether  a species $s$ has expired its decay time for a given expression level $\level{s}$,  we check whether $(z+1) - \refr_s \geq \life_s(\level{s})$ where $z$ is the actual value of the clock. A similar reasoning holds also for reactions. Hence, for each species, instead of storing actual timestamp $t$, we memorize the difference between the actual value of the clock and $t$. Moreover, as this value can still be unbounded, we observe that once it is greater than the maximum time needed to perform a reaction,  its actual value is irrelevant and it can be bounded by the greatest duration of reactions $D = \max\{\dur(\rho) \mid \rho \in \RS\}$. 

More formally, in \rnd each species $s$ is represented by a triple $\tuple{\lev_s, \refr_s, \birth_s}$. We abstract this representation using the following encoding:
$$
\enc{\tuple{\lev_s, \refr_s, \birth_s}} = 
\begin{cases}
\tuple{\lev_s, \omega, \birth'_s}  &\text{if } \lev_s = 0\\
\tuple{\lev_s, (z-\refr_s), \birth'_s}  & \text{otherwise}
\end{cases}
$$
where $\birth'_s[k]=\min((z-\birth_s[k]), D)$ for all $k \in [0..\setlev_s-1]$.

In the following, we denote by $ \inc{D}{\birth}$ the increment by one of all timestamps  in $\birth$: \ie
$\forall k \in [0.. \setlev_s-1]$, $\birth[k] = \min(\birth[k]+1, D)$.
This way, the encoding of a \rnd network $(\res, \RS)$ into a Kripke structure, denoted $K=\enc{(\res, \RS)}$, is defined as follows:

\begin{definition}\label{def:kripke}
Given a \rnd network (\res, \RS) with initial state $(s,\level{s})$ for each $s\in \res$, $\res = \{s_1, \dots, s_n\}$ and $\RS =\{\rho_1, \dots, \rho_m \}$, the corresponding Kripke structure over $A$, $K =(V, v_0, \longrightarrow, \lab)$, is  

\begin{itemize}

 \item the set of states $V$ is a set of tuples $v= (v(s_1), \dots ,v(s_n), v(\rho_1), \dots, v(\rho_m))$. 
Each  $v(s)$ is represented as above as a tuple $\tuple{\lev_s, \refr_s, \birth_s}$ and for each $v(s)$ we take all possible combinations of values in the set 
$$
\begin{array}{ll}
\{\tuple{\lev_s, \refr_s, \birth_s} \mid &\lev_s \in [0..\setlev_s-1], \\
&  \refr_s = \omega \text{ if } \lev_s=0  \text{ or } \refr_s \in [0..\life_s(\lev_s)] \text{ if } \lev_s \neq 0,\\
& \birth_s[k] \in [0..D]\text{ for } k\in [0..\setlev_s-1]\}.
\end{array}
$$% where $\life_s(\lev_s)$ may be different for each level $\lev_s$. 
Analogously, for $v(\rho)$ we take  values in $\{0,1\}$.

\item the initial state $v_0 = (v(s_1), \dots ,v(s_n),v(\rho_1), \dots, v(\rho_m))$ is  defined as: for all $s_j \in \res$,   $v_0(s_j) = \tuple{\level{s_j}, 0, 0^{\setlev_{s_j}}}$ and for all $\rho_k \in \RS$, $v_0(\rho_k) = 1$ .


\item the set of transitions $\longrightarrow \subseteq V \times V$  is defined as
\begin{enumerate}[{Item} 1.]
 \item Encoding of the clock transition: \\
 for each $v\in V$ there exists $v'\in V$ and $v \longrightarrow v'$ such that:
 $$
v'(s_j)=
\begin{cases}
\tuple{\lev_{s_j}, \omega, \inc{D}{\birth_{s_j}}} & \text{if } \lev_{s_j} =0\\
\tuple{\lev_{s_j}, \refr_{s_j} +1, \inc{D}{\birth_{s_j}}} & \text{if } \lev_{s_j} \neq 0  \wedge \refr_{s_j}+1 < \life_{s_j}(\lev_{s_j})\\
\tuple{\lev_{s_j}-1, 0, \inc{D}{\birth_{s_j}}\sub{0}{\lev_{s_j}} } & \text{otherwise.}
\end{cases}
$$
for $s_j\in \res$ and $v'(\rho_k)= 1$ for all $\rho_k \in \RS$.

\item Encoding of reaction transitions:\\
for all $\rho \in \RS$ and for all $v\in V$ such that
\begin{itemize}
 \item $\forall (r, \level{r})\in R$ with $v(r) = \tuple{\lev_r, \refr_r, \birth_r}$: $ \lev_r \geq \level{r} \wedge \birth_r[\level{r}] \geq \dur(\rho)$ and
\item $\forall (i,\level{i})\in I$ with $v(i) = \tuple{\lev_i, \refr_i, \birth_i}$: $\lev_i < \level{i} \wedge \birth_i[\level{i}] \geq \dur(\rho)$ and
 \item  $v(\rho) = 1$;
\end{itemize}
there exists $v' \in V$ and $v \longrightarrow v'$ such that 
\begin{itemize}
 \item $\forall (p, +) \in P$ with  $v(p) = \tuple{\lev_p, \refr_p, \birth_p}$: if $\lev_p = \setlev_p -1$ then $v'(p) = \tuple{\lev_p, 0, \birth_p}$, otherwise  $v'(p) = \tuple{\lev_p+1, 0, \birth_p\sub{0}{\lev_p +1}}$ and 
 \item $\forall (p, -) \in P$ with $v(p) = \tuple{\lev_p, \refr_p, \birth_p}$: if $\lev_p = 0$ then $v'(p) = \tuple{\lev_p, \omega, \birth_p}$, otherwise  $v'(p) = \tuple{\lev_p-1, 0, \birth_p\sub{0}{\lev_p}}$ and
\item $v'(\rho) = 0$;
\end{itemize}
%\item for each $v\in V$ such that there is no $v' \in V$, such that $v \longrightarrow v'$ we add a new transition $v \longrightarrow v$.

\end{enumerate}


\item the labeling function $\lab$ is, for each $v \in V$: $$\lab(v)= \{ (s_j, l) \mid s_j \in \res, v(s_j) = \tuple{\lev_{s_j}, \refr_{s_j}, \birth_{s_j}} \text{ and } 0 \leq l \leq l_{s_j} \}.$$
\end{itemize}


\end{definition}
Notice that for each reaction $\rho \in \RS$, $v(\rho)$ abstracts place $q_{\rho}$ in  \rnd network $(\res, \RS)$. Its role   is to disallow more than one execution of the same reaction in the same time unit: \ie  whenever  $v(\rho)=0$ reaction $\rho$ is disabled (resp. $v(\rho)=1$ reaction is enabled). Moreover this Kripke structure is well defined, in particular $\longrightarrow$ is left total as Item 1 in  Definition \ref{def:kripke}  ensures that for each state there is at least an output transition. 
The encoding of a \rnd network into a Kripke structure is sound and complete as stated by the following theorem. \looseness=-1

\begin{theorem}
Given a \rnd network $(\res, \RS)$, %its encoding 
$\enc{(\res, \RS)}$  is sound and complete.
\end{theorem}
\begin{proof}[Sketch]
We start by proving that the encoding $\enc{\cdot}$ is sound. Hence we will prove that, given a \rnd network $(\res, \RS)$ with initial state $(s, \level{s})$ for each $s \in \res$ and a reachable marking $M'$,  there exist a reachable state $v'$ in $\enc{(\res, \RS)}$ 
s.t. that  $\forall s\in \res$, $v'(s)=\enc{M'(q_s)}$ and $\forall \rho \in \RS$, $v'(\rho) = \min(1, M'(\Pclock)-M'(q_{\rho}))$.
We proceed by induction on the length of the firing sequence, the base case follows by construction.
The inductive step follows by a case analysis on the last fired transition: $\firing{M}{t}{\sigma}{M'}$. By inductive hypothesis there exists a state $v$  s.t.  $v_0 \longrightarrow^* v$ and  $\forall s\in \res$, $v(s)=\enc{M(q_s)}$ and $\forall \rho \in \RS$, $v(\rho) = \min(1, M(\Pclock)-M(q_{\rho}))$, we show that  there exists $v'$ s.t. $v \longrightarrow v'$ and $ \forall s\in \res$, $v'(s)=\enc{M'(q_s)}$ and  $\forall \rho \in \RS$, $v'(\rho) = \min(1, M'(\Pclock)-M'(q_{\rho}))$:
\begin{description}
 \item[$t=t_c$:]  $\forall s \in \res$ let $v(s) = \enc{M(q_s)}$ with  $M(q_s) = \tuple{\lev_s, \refr_s, \birth_s}$, the marking of $q_s$ after the firing  either remains unchanged if $\lev_s = 0 \vee (z+1) -\refr_s < \life(\lev_s)$ or $M'(q_s) = \tuple{\lev_s-1, z+1, \birth_s\sub{z+1}{\lev_s}}$. Item 1 in Definition \ref{def:kripke} guarantees that $v'$ exists, and it is straightforward to see that  $\forall s\in \res$, $v'= \enc{M'(q_s)}$, moreover $\forall \rho \in \RS$, $v'(\rho) = \min(1,M'(\Pclock)-M'(q_{\rho}))= 1$.
 \item[$t=t_{\rho}$:] $\forall s\in \res$ let $v(s) = \enc{M(q_s)}$. As there  exists a $\sigma$ s.t. the firing condition $L(t_{\rho})$ is satisfied,  $v(\rho)=\min(1,M(\Pclock)-M(q_{\rho}))=1$. Moreover $\forall (r, \level{r})\in R_{\rho}$ we have   $v(r)=\tuple{\lev_r, \refr_r, \birth_r} $ and    $\lev_r \geq \level{r} \wedge \birth_r[\level{r}] \geq \dur(\rho)$, and  $\forall (i,\level{i})\in I_{\rho}$ we have $v(i)=\tuple{\lev_i, \refr_i, \birth_i} $ and $\lev_i < \level{i} \wedge \birth_i[\level{i}] \geq \dur(\rho)$. Thus, for Item 2 in Definition \ref{def:kripke} there exists a state $v'$ s.t. $v \longrightarrow v'$ and one can observe that $\forall s\in \res$, $v'(s) = \enc{M'(q_s)}$ and $\forall \rho \in \RS $, $v'(\rho)=\min(1, M'(\Pclock)-M'(q_{\rho}))$.
 \end{description}

 The opposite direction is similar. Given a \rnd network $(\res, \RS)$, for each reachable state $v'$ ($v_0 \longrightarrow^* v'$) in $\enc{(\res, \RS)}$,  there exists a reachable marking $M'$ s.t. $\forall s \in \res$, $v'(s)=\enc{M'(q_s)}$ and $\forall \rho \in \RS$, $v'(\rho)= \min(1,M'(\Pclock)-M'(q_{\rho}))$. The proof follows by induction on the length of the transition sequence. The base case follows by construction. The inductive step is proved by a case analysis on the type of the last performed transition $v \longrightarrow v'$. 
 By inductive hypothesis there exists a reachable marking $M$ s.t. $\forall s \in \res$, $v(s)=\enc{M(q_s)}$ and $\forall \rho \in \RS$,  $v(\rho)= \min(1,M(\Pclock)-M(q_{\rho}))$, as defined in Definition \ref{def:kripke}, we  have two cases:
% Let $\#t_c$ be the number of transitions of the type in Item (1) in Definition \ref{def:kripke} in $v_0 \longrightarrow^* v$. Since those transition correspond to the firing of the clock transition we can assume $M(\Pclock) = \#t_c$. 
% Thus we can explicitly construct the marking of species: let $v(s)= \tuple{\lev_s, \refr_s, \birth_s}$, then $M(q_s)=\tuple{\lev_s, \#t_c - \refr_s, \birth'_s}$ where $\forall k \in [0..\setlev_s]$  $\birth'_s[k]= (#t_c - \birth_s )}$
 \begin{description}
  \item [Item 1:] By construction, $v \longrightarrow v'$ corresponds to a clock transition. Obtaining the marking $M'$ from $M$ is straightforward via  the firing of  $t_c$:  $\firing{M}{t_c}{\sigma}{M'}$.  Moreover it is easy to see that we have $\forall s \in \res$, $v'(s)=\enc{M'(q_s)}$ and $\forall \rho \in \RS$,  $v'(\rho)= \min(1,M'(\Pclock)-M'(q_{\rho}))=1$.
  \item [Item 2:] By construction this corresponds to a reaction transition. By inspecting the values in  $v(\rho)$, $\forall \rho \in \RS$, we find the only reaction $\rho'$ for which  $v(\rho') = 1$ and $v'(\rho')=0$. Obtaining the marking $M'$ from $M$ is straightforward via  the firing of  $t_{\rho'}$:  $\firing{M}{t_{\rho'}}{\sigma}{M'}$. Moreover we can easily see that $\forall s \in \res$, $v'(s)=\enc{M'(q_s)}$ and $\forall \rho \in \RS$,  $v'(\rho)= \min(1,M'(\Pclock)-M'(q_{\rho}))$. \qed
 \end{description}
\end{proof}



